COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(*pascal programs*)
C00023 ENDMK
C⊗;
(*pascal programs*)
(*$E+*)
program junk,unify,subst,replace,copytermlist,copyterm,copyconst,copysym;
(*pascal can't handle things the way it should so we have to invent strange
	names that are all referring to the same thing, in particular, the type
	of the object at hand. Thus,
	alltyps, an indication of the possible atomic types, is actually made
		up of convoluted versions of the type names.
	this idiocy is carried on throughout, which is why you'll see several
	different names that all look similar but had to be different for pascal. *)

TYPE
	(* alltyps are the types of atomic constants *)
	alltyps = (integertyp, realtyp, booleantyp, chartyp, symboltyp);

	termtyps = (variable, constanttyp, funapp);

	term = ↑t1;

	termlist = ↑tl1;

	constant = ↑c1;

	symbol = ↑sym1;

	t1 = record
		case ttyp:termtyps of
			variable: (vr: integer);
			constanttyp: (cnst: constant);
			funapp:   (fname: symbol;
				   args: termlist)
		end;

	tl1 = record
		notempty: boolean;
		first: term;
		rest: termlist
		end;


		(*changed again: a variable is just an integer, serves fine for
			comparison and we never print them out anyway*)

(*	variable = symbol;	*)	(*vars have names and are free, when they 
					get bound they are replaced by other terms*)

(*	variable = ↑v1;

	v1 = record
		bound: boolean;
		pname: symbol;
		case vtyp:alltyps of
			integer: (ival: integer);
			real:    (rval: real);
			boolean: (bval: boolean);
			char:	 (cval: char);
			term:	 (tval: term)
		end;				*)

	c1 = record
		case ctyp:alltyps of
			integertyp: (ival: integer);
			realtyp:    (rval: real);
			booleantyp: (bval: boolean);
			chartyp:    (cval: char);
			symboltyp:  (sval: symbol)
		end;

	sym1 = record
		notempty: boolean;
		firstch: char;
		tail: symbol
		end;

(*	singlesub = ↑ss1;

	ss1 = record
		vr: variable;
		tm: term
		end;

	sub = ↑s1;

	s1 = record
		failed: boolean;
		isempty: boolean;
		first: singlesub;
		rest: sub
		end;
*)

(*Var x1, y1: termlist;
      x2, y2: term;
      s2: sub;
  Begin
	*initialize: s gets the empty substitution*
    new(s);
    s↑.isempty := true;
    s↑.failed := false;
    x1 := x;		(*these are here because they were in fwh's version*
    y1 := y;
    while x1↑.notempty and y1↑.notempty and not(s↑.failed) do
      begin
	termsubst( x1↑.first, s, x2);
	termsubst( y1↑.first, s, y2);
	if x2↑.ttyp = variable
	  then begin
		if y2↑.ttyp = variable
		  then begin
			if not( eqsym(x2↑.vr↑.pname, y2↑.vr↑.pname) )
			   (*pascal can't handle this comparison itself, records,you know*
			  then composesub( s, pair(x2↑.vr, y2));
			   (*if they are the same variable then nothing need be done*
		       end
		  else if occur(x2, y2)
			 then s↑.failed := true
			 else composesub( s, pair(x2↑.vr, y2))
	       end
	  else if y2↑.ttyp = variable
		 then begin
			if occur(y2, x2)
			  then s↑.failed := true
			  else composesub(s, pair(y2↑.vr, x2))
		      end
		 else if x2↑.ttyp = constant
			then begin
			       if y2↑.ttyp = constant
				 then begin
					if not( eqconst(x2↑.cnst, y2↑.cnst) )
					  then s↑.failed := true;
					  (*if they are = nothing need be done*
				      end
				 else if x2↑.cnst↑.ctyp = term
					then begin
					       matchconst(x2↑.const↑.tval, y2, s2);
					       if s2↑.failed
						 then s↑.failed := true
						 else composesub (s, s2)
					     end
					else s↑.failed := true;
					(*any other kind of constant could only
						match with a variable*
			     end
			else (*x2 is a funapp (thus of type term) and y2 is not a variable
			     if y2↑.ttyp = constant
				then begin
				       if y2↑.cnst↑.ctyp = term
					 then begin
						matchconst(y2↑.cnst↑.tval, x2, s2);
						if s2↑.failed
						  then s↑.failed := true
						  else composesub(s, s2)
					      end
					 else s↑.failed := true
				     end
				else (*x2 and y2 are both funapp terms*
				     if eqsym(x2↑.fname, y2↑.fname)
					then begin
						unify(x2↑.args, y2↑.args, s2);
						if s2↑.failed
						  then s↑.failed := true
						  else composesub(s, s2)
					     end
					else s↑.failed :=true;
	x1 := x1↑.rest;
	y1 := y1↑.rest
      end; (*of while*
    if x1↑.notempty or y1↑.notempty then s↑.failed := true
  End; (*of unify*
*)
(*unify side effects its args all over the place, the originals are copied before
the call is made*)
(*
Procedure unify(var x, y: termlist; failed:boolean);
  Var x1, y1: termlist;
      x2, y2: term;
      subfailed: boolean;
  Begin
	(*initialize*
    failed := false;
    x1 := x;
    y1 := y;
    while x1↑.notempty and y1↑.notempty and not(failed) do
      begin
	x2 := x1↑.first;
	y2 := y1↑.first;
	if x2↑.ttyp = variable
	  then begin
		if y2↑.ttyp = variable
		  then x2↑.vr↑.pname := y2↑.vr↑.pname
		    (* if they're already the same, the assignment is unnecessary
		     but cheaper than testing the equality and won't hurt anything*
		  else if occur(x2, y2)
			 then failed := true
			 else subst(x2↑.vr, y2, x, y)
	       end
	  else if y2↑.ttyp = variable
		 then begin
			if occur(y2, x2)
			  then failed := true
			  else subst(y2↑.vr, x2, x, y)
		      end
		 else if x2↑.ttyp = constant
			then begin
			       if y2↑.ttyp = constant
				 then begin
					if not( eqconst(x2↑.cnst, y2↑.cnst) )
					  then failed := true;
					  (*if they are = nothing need be done*
				      end
				 else if x2↑.cnst↑.ctyp = term
					then begin
					       matchconst(x2↑.const↑.tval, y2, x, y, subfailed);
					       if subfailed
						 then failed := true
					     end
					else failed := true;
					(*any other kind of constant could only
						match with a variable*
			     end
			else (*x2 is a funapp (thus of type term) and y2 is not a variable*
			     if y2↑.ttyp = constant
				then begin
				       if y2↑.cnst↑.ctyp = term
					 then begin
						matchconst(y2↑.cnst↑.tval, x2, x, y, subfailed);
						if subfailed
						  then failed := true
					      end
					 else failed := true
				     end
				else (*x2 and y2 are both funapp terms*
				     if eqsym(x2↑.fname, y2↑.fname)
					then begin
						unify(x2↑.args, y2↑.args, subfailed);
						if subfailed
						  then failed := true
					     end
					else failed :=true;
	x1 := x1↑.rest;
	y1 := y1↑.rest
      end; (*of while*
    if x1↑.notempty or y1↑.notempty then failed := true
  End; (*of unify*
*)

(* the true glory of the new type defs shows up here... no matchconst is necessary!
Procedure Matchconst(x, y, allx, ally: term; var failed: boolean);
  Var x1, y1: termlist;
      subfailed: boolean;
  Begin
    failed := false;
    if y↑.ttyp = variable 
      then subst(y↑.vr, x, allx, ally)
      else if y↑.ttyp = constant
	     then begin
		    if not(eqconst(x, y↑.cnst))
		      then failed := true
		  end (*if they're the same then nothing need be done*
	     else if x↑.ttyp = funapp
		    then begin
			   if eqsym(y↑.fname, x↑.fname)
			     then begin
				    x1 := x↑.args;
				    y1 := y↑.args;
				    while x1↑.notempty and y1↑.notempty and not(failed)
				      do begin
					   Matchconst(x1↑.first, y1↑.first, allx, ally, subfailed);
					   if subfailed
					     then failed := true
					 end
				  end
			     else failed := true
			 end
		    else failed := true
  End; (*matchconst*
*)

Function occur(x,y:term):boolean;
begin
occur:= true;
end;


Procedure Replace(x, t: term; var tml: termlist);
  Var tl1:termlist;
	t1:term;
  Begin
    tl1:= tml;
    while tl1↑.notempty do
    begin
      t1 := tl1↑.first;
      if not(t1↑.ttyp = constanttyp)
        then begin
	      if t1↑.ttyp = variable
	      then begin
		     if x↑.vr = t1↑.vr
		       then (*t1 gets t, but i dont think an assignment will work;
				try it anyway, think about it later*)
			    tl1↑.first := t (*need to mung record, not just ptr t1*)
		       (*else, no change needed*)
		   end
	      else (*it's a funapp*)
		   replace (x, t, tl1↑.first↑.args)
	   end;
      (*if its a constant no changes need be made*)
      tl1 := tml↑.rest
    end (*of while*)
  End; (*replace*)

Procedure Subst(x, t:term; var t1, t2:termlist);
Begin
  replace(x, t, t1);
  replace(x, t, t2)
End;


Function Eqsym(x,y:symbol):boolean;
Begin
  while x↑.notempty and y↑.notempty and (x↑.firstch = y↑.firstch) do
    begin
	x:=x↑.tail;
	y:=y↑.tail
    end;
  if x↑.notempty or y↑.notempty
    then eqsym:= false
    else eqsym:= true
End;


Function eqconst(x,y:constant):boolean;
Begin
  if x↑.ctyp = y↑.ctyp
    then case x↑.ctyp of
		integertyp: eqconst:= x↑.ival = y↑.ival;
		realtyp: eqconst:= x↑.rval = y↑.rval;
		booleantyp: eqconst:= x↑.bval = y↑.bval;
		chartyp: eqconst:= x↑.cval = y↑.cval;
		symboltyp: eqconst:= eqsym (x↑.sval, y↑.sval)
	 end
    else eqconst:= false
End;


Function Copysym(oldsym:symbol):symbol;
  Var newsym, lastnode, newnode:symbol;

  Begin
    new(newsym);
    lastnode := newsym;
    while oldsym↑.notempty do
    begin
      lastnode↑.notempty := true;
      lastnode↑.firstch := oldsym↑.firstch;
      new(newnode);
      lastnode↑.tail := newnode;
      lastnode := newnode;
      oldsym := oldsym↑.tail
    end;
    lastnode↑.notempty := false;
    copysym := newsym
  End; (*Copysym*)


Function Copyterm(oldtm:term):Term;
forward;


Function Copytermlist(tml:termlist):Termlist;
  Var newnode, lastnode, tmlnew:termlist;
	
  Begin
    new(tmlnew);
    lastnode := tmlnew;
    while tml↑.notempty do
    begin
      lastnode↑.notempty := true;
      lastnode↑.first := copyterm(tml↑.first);
      new(newnode);
      lastnode↑.rest := newnode;
      lastnode := newnode;
      tml := tml↑.rest;
    end;
    lastnode↑.notempty := false;
    copytermlist := tmlnew
  End; (*copytermlist*)


Function Copyconst(oldconst:constant):Constant;
  Var newconst:constant;

  Begin
    new(newconst);
    newconst↑.ctyp := oldconst↑.ctyp;
    case newconst↑.ctyp of
	integertyp: newconst↑.ival := oldconst↑.ival;
	realtyp: newconst↑.rval := oldconst↑.rval;
	booleantyp: newconst↑.bval := oldconst↑.bval;
	chartyp: newconst↑.cval := oldconst↑.cval;
	symboltyp: newconst↑.sval := copysym(oldconst↑.sval)
    end; (*of case stmt*)
    copyconst := newconst
  End; (*Copyconst*)


Function Copyterm;
  Var newtm:term;

  Begin
    new(newtm);
    newtm↑.ttyp := oldtm↑.ttyp;
    case newtm↑.ttyp of
	variable: newtm↑.vr := oldtm↑.vr; (*it's just an integer*)
	constanttyp: newtm↑.cnst := copyconst(oldtm↑.cnst);
	funapp:   begin
		    newtm↑.fname := copysym(oldtm↑.fname);
		    newtm↑.args := copytermlist(oldtm↑.args)
		  end
    end; (*of case stmt*)
    copyterm := newtm
  End; (*Copyterm*)							


(*the first call on unify will repeat the arglists being unified- dumb, but it
makes it possible to accomplish the substitutions by replacement as we go instead
of building a substitution and making new copies of everything every time we do
a substitution.  the allx and ally args are necessary to ensure that any replacements
resulting from recursive calls get made throughout the entire termlists you started
with*)
Procedure unify(var x, y, allx, ally: termlist; failed:boolean);
  Var x1, y1: termlist;
      x2, y2: term;
      subfailed: boolean;
  Begin
	(*initialize*)
    failed := false;
    x1 := x;
    y1 := y;
    while x1↑.notempty and y1↑.notempty and not(failed) do
      begin
	x2 := x1↑.first;
	y2 := y1↑.first;
	if x2↑.ttyp = variable
	  then begin
		if y2↑.ttyp = variable
		  then x2↑.vr := y2↑.vr
		    (* if they're already the same, the assignment is unnecessary
		     but cheaper than testing the equality and won't hurt anything*)
		  else if occur(x2, y2)
			 then failed := true
			 else subst(x2, y2, x, y)
	       end
	  else if y2↑.ttyp = variable
		 then begin
			if occur(y2, x2)
			  then failed := true
			  else subst(y2, x2, x, y)
		      end
		 else if x2↑.ttyp = constanttyp
			then begin
			       if y2↑.ttyp = constanttyp
				 then begin
					if not( eqconst(x2↑.cnst, y2↑.cnst) )
					  then failed := true;
					  (*if they are = nothing need be done*)
				      end
				 else failed := true
			     end
			else (*x2 is a funapp and y2 is not a variable*)
			     if y2↑.ttyp = constanttyp
				then failed := true
				else (*x2 and y2 are both funapp terms*)
				     if eqsym(x2↑.fname, y2↑.fname)
					then begin
						unify(x2↑.args, y2↑.args,
							allx, ally, subfailed);
						if subfailed
						  then failed := true
					     end
					else failed :=true;
	x1 := x1↑.rest;
	y1 := y1↑.rest
      end; (*of while*)
    if x1↑.notempty or y1↑.notempty then failed := true
  End; (*of unify*)

begin (*junk*)
end.